basic
IsEqFun(T;eq) == x, y:T. ((x eq y))  (x = y) 

latex

---

clarification:

basic
IsEqFun(T;eq) == x:T, y:T. ((x eq y))  (x = y  T) 

latex

Up	rel 1, rel 1
Wellformedness Lemmas	eqfun p wf, eqfun p wf
Definitions	x:A. B(x), P  Q, b, x f y, s = t
FDL editor aliases	eqfun_p